\begin{tabbing}
(\=(((CaseNat 0 `j') \+
\\[0ex]CollapseTHEN (((Reduce 0) 
\\[0ex]CollapseTHEN ((Try (Trivial))$\cdot$))$\cdot$))$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN (((((CaseNat 1 `j') 
\\[0ex]CollapseTHEN (((Reduce 0) 
\\[0ex]CollapseTHEN ((Try (
\-\\[0ex]T\=rivial))$\cdot$))$\cdot$))$\cdot$) \+
\\[0ex]CollapseTHEN (Auto'))$\cdot$))$\cdot$
\-
\end{tabbing}